Bahasa pengaturcaraan notasi Z (disebut umumnya zed, dinamakan sempena teori set Zermelo-Fränkel) ialah bahasa spesifikasi rasmi yang digunakan bagi mengambar dan memodelkan atur cara komputer. Ia disasarkan bagi spesifikasi jelas atur cara komputer dan pembentukan bukti mengenai tabiat atur cara berkenaan.Z pada asalnya dicadangkan oleh Jean-Raymond Abrial pada tahun 1977 dengan bantuan Steve Schuman dan Bertrand Meyer .[1] Ia dimajukan dengan lebih lanjut oleh Programming Research Group di Universiti Oxford, di mana Abrial bertugas pada awal lapan puluhan.
Sungguhpun notasi Z menggunakan banyak simbol bukan ASCII, spesifikasi termasuk cadangan menukar simbol notasi Z kepada ASCII dan pada LaTeX.
Sumber berguna bagi pengguna baru yang berminat mempelajari Z ialah The Z Notation: a reference manual.Notasi Z digunakan pada projek CICS IBM.